Iof proof for Lemma connex functionality wrt implies:
1. T : Type
2. R : T
T
3. R' : T
T
4.
x, y:T. R(x,y) 
R'(x,y)
5.
x, y:T. R(x,y) 
R(y,x)
6. x : T
7. y : T
R'(x,y) R'(y,x)
by ((ReplaceWith x, y:T. {R(x,y) R'(x,y)} 4)
CollapseTHENA (((Unfold `guard` 0)
CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t
C) inil_term)))
))
C1:
C1: 4. x, y:T. {R(x,y) R'(x,y)}
C1: 5. x, y:T. R(x,y) R(y,x)
C1: 6. x : T
C1: 7. y : T
C1: R'(x,y) R'(y,x)
C.